北京邮电大学学报 ›› 2005, Vol. 28 ›› Issue (4): 45-49.doi: 10.13190/jbupt.200504.45.zhangdm
基于Uppaal的移动IPv6协议的模型检测
张冬梅,马华东,高大永
- 北京邮电大学 计算机科学与技术学院, 北京 100876
Automatic Verification of Mobile IPv6 Using Uppaal
HANG Dongmei,MA Huadong,GAO Dayong
- School of Computer Science and Technology, Beijing University of Posts and Telecommunications, Beijing 100876, China
摘要:
采用形式化方法对移动IPv6协议系统建立了时间自动机模型,使用实时模型检测工具Uppaal对所建模型的关键性质:活性、移动性和平滑切换等进行了分析和检测. 检测结果证明,移动IPv6协议在切换时存在丢包现象. 通过分析丢包产生的原因,提出了移动IPv6实现平滑切换的理想时间约束条件,并在理想条件下重新验证了协议的性质. 结合模型在理想约束条件下的检测结果指出了提高移动IPv6移动性能的设想.